\begin{tabbing}
$\forall$\=$i$, $x$:Id, $T$:Type, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $f$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow$DeclaredType(${\it ds}$;$x$)), $k$:Knd,\+
\\[0ex]$A$:Realizer.
\-\\[0ex]R{-}Feasible($A$)
\\[0ex]$\Rightarrow$ $\neg$R{-}occurs($A$;$i$;$x$)
\\[0ex]$\Rightarrow$ ${\it ds}$ $\parallel$ R{-}ds($A$;$i$)
\\[0ex]$\Rightarrow$ $k$ : $T$ $\parallel$ R{-}da($A$;$i$)
\\[0ex]$\Rightarrow$ (isrcv($k$) $\Rightarrow$ R{-}da($A$;source(lnk($k$)))($k$)?Void $\subseteq\rho$ $T$)
\\[0ex]$\Rightarrow$ $\neg$write{-}restricted($A$;$i$;$k$)
\\[0ex]$\Rightarrow$ ($\forall$$y$:Id. $y$ $\in$ dom(${\it ds}$) $\Rightarrow$ $\neg$read{-}restricted($A$; $i$; $y$))
\\[0ex]$\Rightarrow$ @$i$ effect $k$(v:$T$)  $x$ := $f$ State(${\it ds}$) v  $\parallel$ $A$
\end{tabbing}